T:Type, L1, L2, L:T List.
disjoint_sublists(T;L1;L2;L)
 (f:((||L1||+||L2||)||L||).
 (Inj((||L1||+||L2||); ||L||; f)
 (& (i:(||L1||+||L2||).
 (& ((i<||L1||  L1[i] = L[f(i)]  T) & (||L1||i  L2[i-||L1||] = L[f(i)]  T))) 

latex

Definitions	P & Q, x:A. B(x), disjoint_sublists(T;L1;L2;L), t  T, x:A. B(x), {i..j}, Inj(A; B; f), P  Q, False, A, AB, ||as||, i<j, if b t else f fi, i  j < k, Prop, True, b, b, ij, , T, P  Q, P  Q, Unit, ij, l[i], {T}, SQType(T),
Lemmas	increasing inj, inject wf, select wf, non neg length, ifthenelse wf, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, lt int wf, bool wf, le int wf, le wf, assert wf, bnot wf, int seg wf, length wf1, disjoint sublists wf